(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(set-info :status unsat)
(set-info :category "industrial")
(set-info :source |
  Generated using using the Low-Level Bounded Model Checker LLBMC.
  C files used in the paper: Florian Merz, Stephan Falke, Carsten Sinz: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. VSTTE 2012: 146-161
|)
(declare-fun n_0x1088070 () (_ BitVec 32))
(assert
(let ((?x1 (_ bv0 32)))
(let ((?x2 (_ bv1048576 32)))
(let ((?x3 (_ bv0 64)))
(let ((?x4 (_ bv24 64)))
(let ((?x5 (_ bv542113792 64)))
(let ((?x6 (_ bv1605369856 64)))
(let ((?x7 (_ bv9223372036854775808 64)))
(let ((?x8 (_ bv536870912 64)))
(let ((?x9 n_0x1088070))
(let (($x10 (bvsgt ?x9 ?x1)))
(let (($x11 (bvsle ?x9 ?x2)))
(let (($x12 (and $x10 $x11)))
(let ((?x13 ((_ sign_extend 32) ?x9)))
(let ((?x14 (bvmul ?x13 ?x4)))
(let (($x15 (bvugt ?x14 ?x3)))
(let (($x16 (bvule ?x14 ?x6)))
(let (($x17 (and $x15 $x16)))
(let (($x18 (not $x12)))
(let (($x19 (or $x18 $x17)))
(let (($x20 (not $x19)))
(let (($x21 (and $x12 $x17)))
(let ((?x22 ((_ sign_extend 32) ?x9)))
(let ((?x23 (bvmul ?x4 ?x22)))
(let ((?x24 (bvadd ?x5 ?x23)))
(let (($x25 (bvule ?x24 ?x8)))
(let ((?x26 (bvadd ?x5 ?x14)))
(let (($x27 (bvule ?x24 ?x26)))
(let (($x28 (and $x12 $x27)))
(let (($x29 (or $x25 $x28)))
(let ((?x30 ((_ zero_extend 1) ?x5)))
(let ((?x31 ((_ zero_extend 1) ?x23)))
(let ((?x32 (bvadd ?x30 ?x31)))
(let ((?x33 ((_ extract 64 64) ?x32)))
(let (($x34 (= ?x33 (_ bv1 1))))
(let (($x35 (not $x34)))
(let (($x36 (and $x29 $x35)))
(let (($x37 (= ?x23 ?x3)))
(let (($x38 (or $x36 $x37)))
(let (($x39 (bvule ?x23 ?x7)))
(let (($x40 (and $x38 $x39)))
(let (($x41 (not $x21)))
(let (($x42 (or $x41 $x40)))
(let (($x43 (not $x42)))
(let (($x44 (or $x20 $x43)))
$x44
))))))))))))))))))))))))))))))))))))))))))))
)
(check-sat)
(exit)
